A, B:Realizer. R-Feasible(A)  R-Feasible(B)  A || B  R-discrete(A) || R-discrete(B) 

latex

Definitions

x. t(x), Top, R-discrete(R), , P & Q, i  j , False, A, A  B, {T}, SQType(T), , t  T, P  Q, x:A. B(x), x(s), A c B, Dec(P), P  Q, ff, tt, P  Q, if b then t else f fi , Y, , A || B

Lemmas

R-size-base, fpf-compatible-symmetry, fpf-compatible-join, R-compat-Rplus2, fpf-join wf, Rplus-right wf, Rplus-left wf, R-discrete wf, id-deq wf, product-deq wf, Id wf, decidable assert, R-Feasible-Rplus, Rplus-implies, R-size-decreases, decidable le, decidable cand, nat wf, ge wf, nat properties, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, bool sq, Rplus? wf, bool cases, R-compat-discrete-base, le wf, es realizer wf, R-Feasible wf, R-compat wf, nat plus wf, R-size wf